Lemma successors_equal_implies_equal:
  forall a b, S a = S b -> a = b.
Proof.
  intros a b H.
  inversion H.
  reflexivity.
Qed.